COMMENT ⊗   VALID 00002 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	VAR: x,y,z,u,v,w
 00003 ENDMK
⊗;
VAR: x,y,z,u,v,w;
PRE_PRED: T,C,S,A;

A1: S(x,y,y,x);
A2: S(u,v,x,y)⊃S(x,y,u,v);
A3: S(u,v,x,y)⊃S(v,u,x,y);
A4: T(x,y,z)⊃T(y,z,x);
A5: T(x,y,z)⊃T(y,x,z);
A6: C(u,v,w,x,y,z)⊃(A(u,v,w,x,y,z)∧A(v,u,w,y,x,z)∧A(u,w,v,x,z,y));
A7: (T(u,v,w)∧T(x,y,z)∧S(u,v,x,y)∧S(v,w,y,z)∧S(u,w,x,z))⊃
            C(u,v,w,x,y,z);
THM:(T(x,y,z)∧S(x,z,y,z))⊃A(z,x,y,z,y,x);;